T:Type, R:(TTprop{i:l}). SWellFounded(x R y)  SWellFounded(x rel_plus(T; R) y) 

latex

Definitions	x:A. B(x), prop{i:l}, P  Q, SWellFounded(R(x;y)), x f y, x:A. B(x), , t  T, A  B, A, False, sq_type(T), guard(T), rel_exp(T; R; n), Y, if b then t else f fi , tt, ff, P  Q, rel_plus(T; R), , decidable(P), P  Q, (i = j), , Unit, P  Q,
Lemmas	nat plus properties, nat wf, rel exp wf, le wf, decidable int equal, nat plus wf, rel plus wf, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff